/*******************************************************************\

Module: Program Transformation

Author: Daniel Kroening, kroening@kroening.com

** Modified by YU-WEI LEE

\*******************************************************************/

#include <std_expr.h>

#include <arith_tools.h>

#include <langapi/language_util.h>

#include "goto_program.h"

#include <sstream>

//#include "../wolverine/princess/princess_interface.h"

//#include <cfa/cfa.h>

//#include <cfa/typedef.h>

// added: output to CFA
extern std::map<std::string, std::map<std::string, std::string> > struct_info;
extern void RecursiveGetMember( 
map<string, map<string, string> > m,  
map<string, map<string, string> >::iterator it_m, \
vector<string> &result \
);

Expr* goto_programt::handle_symCFA(
  const class namespacet &ns,
  const irep_idt &identifier, 
  const exprt& e) const
{
  Expr* result = new VarExpr;
  char * cstr;
  cstr = new char [(e.get("identifier").as_string().size())+1];
  strcpy( cstr, e.get("identifier").as_string().c_str() );
  char *delim = "::";
  char * pch;
  pch = strtok( cstr, delim );
  while( pch != NULL )
  {
    //cout << pch << endl;
    strcpy(((VarExpr*)result)->x, pch);
    pch = strtok( NULL, delim );
  }
  //strcpy( ((VarExpr*)result)->x, e.get("identifier").as_string().c_str() );
  //cout << "Symbol created: " << ((VarExpr*)result)->x << endl;
  return result;
}

Prop* goto_programt::handle_propCFA( 
const class namespacet &ns,
const irep_idt &identifier,
const exprt &e ) const
{
  //cout << "Proposition handling:" << e.id() << endl;
  if( e.id() == "symbol" )
  {
    /*Expr *r_e1 = handle_symCFA(ns, identifier, e);
    Expr *r_e2 = new IntExpr;
    ((IntExpr*)r_e2)->i = 0;
    Prop* result = new InequProp;
    ((InequProp*)result)->e1 = r_e1;
    ((InequProp*)result)->e2 = r_e2;
    ((InequProp*)result)->p = GT;
    return result;*/
    //cout << "e = " << e << endl;
    //cout << "X: Symbol not supported in proposition handling." << endl;
    cout << "UNKNOWN" << endl;
    exit(0);
  }
  else if( e.id()=="constant" )
  {
    //cout << "X: Constant not supported in proposition handling." << endl;
    // Treat it as boolean variable
    Prop * result = new BoolProp;
    if (e.type().id() == "bool") {
       if( e.get_string("value") == "false" )
       {
         ((BoolProp*)result)->b = 0;
       }
       else
       {
         ((BoolProp*)result)->b = 1;
       }
    }
    else
    {
      mp_integer mi;
      to_integer(e, mi);
      int a = ((int)( mi.to_long() ));
      ((BoolProp*)result)->b = a;
      //cout << "Constant boolean value:" << a << endl;
    }
    //cout << "Boolean value:" << ((BoolProp*)result)->b << endl;
    return result;
  }
  else if( e.id()=="if")
  {
    //cout << "IF proposition not yet supported." << endl;
    Prop * result = new BinProp;
    ((BinProp *)result)->l = And;
    Prop * result1 = new BinProp;
    ((BinProp *)result1)->l = Imp;
    ((BinProp *)result1)->p1 = handle_propCFA( ns, identifier, e.op0() );
    ((BinProp *)result1)->p2 = handle_propCFA( ns, identifier, e.op1() );
    Prop * result2 = new BinProp;
    ((BinProp *)result2)->l = Imp;
    Prop * result2A = new NegProp;
    ((NegProp *)result2A)->p = handle_propCFA( ns, identifier, e.op0() );
    ((BinProp *)result2)->p1 = result2A;
    ((BinProp *)result2)->p2 = handle_propCFA( ns, identifier, e.op2() );
    ((BinProp *)result)->p1 = result1;
    ((BinProp *)result)->p2 = result2;
    return result;
  }
  else if( e.id()=="=" || e.id()=="notequal" ||
          e.id()=="<" || e.id()==">" || e.id()=="<=" || e.id()==">=" )
  {
    //cout << "Prop: comparisons" << endl;
    // see operator
    if( e.id() == "<" )
    {
      Prop * result = new InequProp;
      ((InequProp *)result)->p = LT;
      ((InequProp *)result)->e1 = handle_exprCFA(0, ns, identifier, e.op0());
      ((InequProp *)result)->e2 = handle_exprCFA(0, ns, identifier, e.op1());
      return result;
    }
    else if( e.id() == ">" )
    { 
      Prop * result = new InequProp;
      ((InequProp *)result)->p = GT;
      ((InequProp *)result)->e1 = handle_exprCFA(0, ns, identifier, e.op0());
      ((InequProp *)result)->e2 = handle_exprCFA(0, ns, identifier, e.op1());
      return result;
    }
    else if( e.id() == "=")
    {
      //if((e.op0()).get("identifier").as_string().compare(2,7,"CPROVER") == 0 ){
      //if((e.op0()).get("identifier").as_string().compare("__CPROVER_alloc_size") == 0 ){
      //    cout << "GETGET: " <<(e.op0()).get("identifier").as_string() << endl;
      //}
      Prop * result = new InequProp;
      ((InequProp *)result)->p = Eq;
      ((InequProp *)result)->e1 = handle_exprCFA(0, ns, identifier, e.op0());
      ((InequProp *)result)->e2 = handle_exprCFA(0, ns, identifier, e.op1());
      return result;
    }
    else if( e.id() == "notequal" )
    {
      Prop * result = new NegProp;
      Prop * result2 = new InequProp;
      ((InequProp *)result2)->p = Eq;
      ((InequProp *)result2)->e1 = handle_exprCFA(0, ns, identifier, e.op0());
      ((InequProp *)result2)->e2 = handle_exprCFA(0, ns, identifier, e.op1());
      ((NegProp *)result)->p = result2;
      return result;
    }
    else if( e.id() == ">=" )
    {
      Prop * result = new NegProp;
      Prop * result2 = new InequProp;
      ((InequProp *)result2)->p = LT;
      ((InequProp *)result2)->e1 = handle_exprCFA(0, ns, identifier, e.op0());
      ((InequProp *)result2)->e2 = handle_exprCFA(0, ns, identifier, e.op1());
      ((NegProp *)result)->p = result2;
      return result;
    }
    else if( e.id() == "<=" )
    {
      Prop * result = new NegProp;
      Prop * result2 = new InequProp;
      ((InequProp *)result2)->p = GT;
      ((InequProp *)result2)->e1 = handle_exprCFA(0, ns, identifier, e.op0());
      ((InequProp *)result2)->e2 = handle_exprCFA(0, ns, identifier, e.op1());
      ((NegProp *)result)->p = result2;
      return result;
    }
    Prop * result = new InequProp;
    return result; 
  }
  else if( e.id()=="not" )
  {
    //cout << "Prop: not" << endl;
    Prop * result = new NegProp;
    ((NegProp *)result)->p = handle_propCFA(ns, identifier, e.op0());
    return result;
  }
  else if( e.id()=="and" || e.id()=="or" )
  {
    Prop *result = new BinProp;
    ((BinProp*)result)->p1 = handle_propCFA(ns, identifier, e.op0());
    ((BinProp*)result)->p2 = handle_propCFA(ns, identifier, e.op1());
    if(e.id() == "and"){
        ((BinProp*)result)->l = And;
    }
    else{
        ((BinProp*)result)->l = Or;
    }
    //cout << "X: and/or not supported in proposition handling." << endl;
  }
  /*else if( e.id()=="+" || e.id()=="-" || e.id()=="*" ||
            e.id()=="/" || e.id()=="mod" ||
            e.id()=="bitand" || e.id()=="bitor" || e.id()=="bitxor" )
  {
    //cout << "X: +-*\/mod binand bitor bitxor not supported in proposition handling." << endl;
    //handle_propCFA( ns, identifier, e.op0() );
    //handle_propCFA( ns, identifier, e.op1() );
    exit(0);
  }*///quake
  /*else if( e.id()=="with" &&
           (e.type().id()=="array" || e.type().id()=="mathint") )
  {
    cout << "x: with** array mathint NOT SUPPORTED in proposition handling" << endl;
    //exit(0);
  }*///quake
  /*else if(e.id()=="index")
  {
    cout << "This instruction contains a index which is NOT SUPPORTED in proposition hadling." << endl;
    //exit(0);
  }*///quake
  /*else if(e.id()=="with" && e.type().id()=="struct")
  {
    cout << "X: with/struct not supported in proposition handling." << endl;
    //exit(0);
  }*///quake
  /*else if(e.id()=="member")
  {
    cout << "This instruction contains member call(->) which is NOT SUPPORTED YET in proposition handling" << endl;
    //exit(0);
  }
  else if(e.id()==ID_pointer_offset)
  {
    cout << "This instruction contains ID pointer offset which is  NOT SUPPORTED in proposition handling yet." << endl;
    //exit(0);
  }
  else if(e.id()==ID_address_of)
  {
    cout << "This instruction containts ' ID address of' which is  NOT SUPPORTED in proposition handling yet." << endl;
    //exit(0);
  }
  else if(e.id()=="nondet_symbol" || e.id()=="boundVar")
  {
    cout << "X: nondet symbol / boundVar:  NOT SUPPORTED in proposition handling yet" << endl;
    //exit(0);
  }
  else if(e.id()=="array_of")
  {
    cout << "X: Arrat of:  NOT SUPPORTED in proposition handling yet." << endl;
    //exit(0);
  }*///quake
  else if(e.id()=="exists" || e.id()=="forall")
  {
    //cout << "X: exists / forall:  NOT SUPPORTED in proposition handling yet." << endl;
    cout << "UNKNOWN" << endl;
    exit(0);
  }
  /*else if(e.id()=="lshr" || e.id()=="ashr")
  {
    cout << "X: lshr / ashr:  NOT SUPPORTED in proposition handling yet." << endl;
    exit(0);
  }*/
  /*else if(e.id()=="shl")
  {
    cout << "X: shl:  NOT SUPPORTED in proposition handling yet." << endl;
    //exit(0);
  }*///quake
  /*else if(e.id()=="unary-")
  {
    cout << "This instruction contains unary- which is  NOT SUPPORTED in proposition handling yet." << endl;
    //exit(0);
  }*///quake
  else if(e.id()=="typecast" )
  {
    if( e.type().id() == "bool" )
    {
      Prop * result = new InequProp;
      Expr * result2 = new IntExpr;
      ((IntExpr*)result2)->i = 0;
      ((InequProp *)result)->p = GT;
      ((InequProp *)result)->e1 = handle_exprCFA(0, ns, identifier, e.op0());
      ((InequProp *)result)->e2 = result2;    
      return result;    
    }
    else
    {
      //cout << "This instruction contains a typecast(possibly implicit) with a specific type which is NOT SUPPORTED in proposition handling yet. type:" << e.type().id() << endl;//quake
      cout << "UNKNOWN" << endl;
      exit(0);
    }
  }
  /*else if(e.id()=="abs")
  {
    cout << "This instruction contains abs which is  NOT SUPPORTED in proposition handling yet." << endl;
    //exit(0);
  }*///quake
  /*else if(e.id()=="width")
  {
    cout << "X: width:  NOT SUPPORTED in proposition handling yet." << endl;
    //exit(0);
  }*///quake
  else
  {
    //cout << "WARNING: empty porposition e.id: " << e.id() << endl;
    cout << "UNKNOWN" << endl;
  }
  Prop * empty_result = new BoolProp;
  ((BoolProp *)empty_result)->b = false;
  return empty_result; 
}

Expr* goto_programt::handle_exprCFA( 
const int flag,
const class namespacet &ns,
const irep_idt &identifier,
const exprt &e ) const
{
  //cout << "Expression handling:" << e.id() << endl;
  //assert(!e.is_nil());
  if( e.id() == "symbol" )
  {
    return handle_symCFA(ns, identifier, e);
  }
  else if( e.id()=="constant" )
  {
    Expr* result = new IntExpr;
    if (e.type().id() == "bool") {
       if( e.get_string("value") == "false" )
       {
         ((IntExpr*)result)->i = 0;
       }
       else
       {
         ((IntExpr*)result)->i = 1;
       }
    }
    else if(e.type().id() =="c_enum"){
        //string s_test = e.get("value").as_string();
        mp_integer mi;
        to_integer(e, mi);
        int a = ((int)( mi.to_long() ));
        ((IntExpr*)result)->i = a;
    }
    else
    {
      mp_integer mi;
      to_integer(e, mi);
      int a = ((int)( mi.to_long() ));
      ((IntExpr*)result)->i = a;
      //cout << "Constant value:" << a << endl;
    }
    return result;
  }
  /*else if( e.id()=="=" || e.id()=="notequal" ||
          e.id()=="<" || e.id()==">" || e.id()=="<=" || e.id()==">=" )
  {
    cout << "This instruction containts expression with  comparision which is not YET SUPPORTED." << endl;
    //exit(0);
  }*///quake
  /*else if( e.id()=="not" )
  {
    cout << "This instruction containts expression with not(~) which is NOT YET SUPPORTED." << endl;
    //exit(0);
  }*///quake
  /*else if( e.id()=="and" || e.id()=="or" )
  {
    cout << "Expr::This instruction containts expression with  and/or which is NOT YET SUPPORTED" << endl;
    //exit(0);
  }*///quake
  else if( e.id()=="+" || e.id()=="-" || e.id()=="*" ||
            e.id()=="/" || e.id()=="mod" ||
            e.id()=="bitand" || e.id()=="bitor" || e.id()=="bitxor" )
  {
    //cout << "Expr: +-*/mod binand bitor bitxor" << endl;
    Expr * result = new BinExpr;
    ((BinExpr *)result) -> e1 = handle_exprCFA( 0, ns, identifier, e.op0() );
    ((BinExpr *)result) -> e2 = handle_exprCFA( 0, ns, identifier, e.op1() );
    if( e.id() == "+" ) ((BinExpr *)result) -> op = Plus;
    else if( e.id() == "-" ) ((BinExpr *)result) -> op = Minus;
    else if( e.id() == "*" ) ((BinExpr *)result) -> op = Multi;
    else if( e.id() == "/" ) ((BinExpr *)result) -> op = Divide;
    //else if( e.id() == "bitand" ) ((BinExpr *)result) -> op = Bitand;
    //else if( e.id() == "bitor" ) ((BinExpr *)result) -> op = Bitor;
    //else if( e.id() == "bitxor" ) ((BinExpr *)result) -> op = Bitxor;
    //else if( e.id() == "mod" ) ((BinExpr *)result) -> op = Mod;
    else
    {
      //cout << "WARNING: we Currently only support +/-/*/divide e.id:" << e.id() << endl;
      cout << "UNKNOWN" << endl;
      exit(0);
    }
    return result;
  }
  else if( e.id()=="with" &&
           (e.type().id()=="array" || e.type().id()=="mathint") )
  {
    //cout << "This instruction containts expression with  with,  array, mathint NOT YET SUPPORTED." << endl;
    cout << "UNKNOWN" << endl;
    exit(0);
  }
  else if(e.id()=="index")
  {
    //cout << "This instruction contains a expression with index which is NOT YET SUPPORTED" << endl;
    cout << "UNKNOWN" << endl;
    exit(0);
  }
  else if(e.id()=="with" && e.type().id()=="struct")
  {
    //cout << "Expr: with/struct NOT YET SUPPORTED" << endl;
    cout << "UNKNOWN" << endl;
    //const with_exprt with_struct = to_with_expr(e);
    exit(0);
  }
  else if(e.id()=="member")
  {
    /*forall_named_irep(it_member, e.get_named_sub()){
        //if(it_member->first == "i"){
        //    cout << "first = " << it_member->first << " second = " << it_member->second << endl;
        //}
        if(it_member->first == "operand"){
            cout << "first = " << it_member->first << " second = " << it_member->second << endl;
        }
    }*/
    if(e.op0().id() == "symbol"){
        const member_exprt &struct_member = to_member_expr(e);
        const exprt &from_struct = struct_member.struct_op();

        //const struct_typet struct_type = to_struct_type(from_struct.type());
        //const unsigned component_number =
        //    struct_type.component_number(struct_member.get_component_name());
        string member_s = from_struct.get("identifier").as_string();
        int posx, countx;
        //posx = 0; countx =0;
        for(posx = 0, countx = 0; posx < member_s.size(); posx++){
            if(member_s[posx] == ':'){ countx=countx+1; }
	    if(countx==8){ posx=posx+1 ;break; }
        }
        string tem_s = member_s.substr(posx);
        std::string tem_t = struct_member.get_component_name().c_str();
        string combine = tem_s+".";
        combine = combine + tem_t;
        //cout << "combine1 = " << combine << endl;
        Expr* result = new VarExpr;
        strcpy(((VarExpr*)result)->x, combine.c_str());
        return result;
    }
    else if(e.op0().id() == "dereference"){
        const member_exprt &struct_member = to_member_expr(e);
        const exprt &from_struct = struct_member.struct_op();

        std::string tem_t = struct_member.get_component_name().c_str();
        std::string member_s = e.op0().op0() .get("identifier").c_str();
        int posx, countx;
        for(posx = 0, countx = 0; posx < member_s.size(); posx++){
            if(member_s[posx] == ':'){ countx=countx+1; }
	    if(countx==8){ posx=posx+1 ;break; }
        }
        string tem_s = member_s.substr(posx);
        string combine = tem_s+"->";
        combine = combine + tem_t;
        //cout << "combine2 = " << combine << endl;
        //cout << "This instruction contains a \"call to a member(->)\" operator but this is NOT YET SUPPORTED" << endl;
        cout << "UNKNOWN" << endl;
      
        //cout << " e = " << e.op0().op0() .get("identifier") << endl;
    }
    else{
    }
    //cout << "fromstruct = " << tem_s << endl; 
    //cout << "component name = " << struct_member.get_component_name() << endl;
    //cout << "select(";
    //lineariseExpr(from_struct);
    //cout << "," << component_number << ")";
    //cout << "e = " << e << endl;
    //cout << "e = " << e.get("identifier").as_string() << endl;//nil
    //cout << "e=identifier = " << e.identifier() << endl;
    //exit(0);
  }
  else if(e.id()==ID_pointer_offset)
  {
    //cout << "This instrution contains a ID pointer offset which is not supported yet." << endl;
    cout << "UNKNOWN" << endl;
    exit(0);
  }
  else if(e.id()==ID_address_of) 
  {
    //cout << "This instruction contains a  ID address of which is not supported yet." << endl;
    cout << "UNKNOWN" << endl;
    exit(0);
  }
  else if(e.id()=="nondet_symbol" || e.id()=="boundVar")
  {
    //cout << "Expr: nondet symbol / boundVar: not supported yet" << endl;
    cout << "UNKNOWN" << endl;
    exit(0);
  }
  else if(e.id()=="array_of") 
  {
    if(flag == 2){
        //cout << "Expr: Array of this is  not supported yet." << endl;
        cout << "UNKNOWN" << endl; exit(0);
    }
    //exit(0); // ARRAY OF IS ADDED BY CPROVER in preprocessing, do not add this back if you want to see the result for original code
  }
  /*else if(e.id()=="exists" || e.id()=="forall")
  {
    cout << "Expr have exists / forall: not supported yet." << endl;
    //exit(0);
  }*///quake
  else if(e.id()=="lshr" || e.id()=="ashr") 
  {
    //cout << "Expr have  lshr / ashr: not supported yet." << endl;
    cout << "UNKNOWN" << endl;
    exit(0);
  }
  else if(e.id()=="shl") 
  {
    Expr * result = new BinExpr;
    ((BinExpr *)result) -> e1 = handle_exprCFA( 0, ns, identifier, e.op0() );
    ((BinExpr *)result) -> op = Multi;
    Expr *temp_e = handle_exprCFA( 0, ns, identifier, e.op1() );
    int i1, i2;
    for(i1 = 0, i2 = 1; i1 < ((IntExpr*)temp_e)->i; i1++){
        i2 = i2 * 2;
    }
    ((BinExpr *)result) -> e2 = new IntExpr;
    ((IntExpr*)(((BinExpr *)result) -> e2))->i = i2;
    return result;
    //cout << "temp = " << ((IntExpr*)temp_e)->i << " i2 = " << i2 << endl;
    //((BinExpr *)result) -> e2 = 
    //cout << "shl operator is not supported yet." << endl;
    //exit(0);
  }
  else if(e.id()=="unary-") 
  {
    Expr * result = new BinExpr;
    Expr * result2 = new IntExpr;
    ((IntExpr*)result2)->i = -1;
    ((BinExpr *)result) -> e1 = result2;
    ((BinExpr *)result) -> e2 = handle_exprCFA( 0, ns, identifier, e.op0() );
    ((BinExpr *)result) -> op = Multi;
    //cout << "Expr: unary-: not supported yet." << endl;
    //exit(0);
    return result;
  }
  else if(e.id()=="typecast" ) 
  {
    if(e.type().id() == "signedbv"){
        //ignore 
    }
    else if(e.type().id() == "unsignedbv"){
        //ignore 
    }
    else{
        //cout << "This instruction contains a Typecast(possibly implicit) to " << e.type().id() <<" which is not supported yet." << endl;
        cout << "UNKNOWN" << endl;
        exit(0);
    }
  }
  /*else if(e.id()=="abs") 
  {
    cout << "Expr: abs: not supported yet." << endl;
    //exit(0);
  }*///quake
  /*else if(e.id()=="width") 
  {
    cout << "Expr: width: not supported yet." << endl;
    //exit(0);
  } *///quake
  else
  {
    //cout << "WARNING EMTPY expression. e.id: " << e.id() << endl;
    //cout << "UNKNOW16" << endl;
  }
  Expr * empty_result = new IntExpr;
  ((IntExpr *)empty_result)->i = 0;
  return empty_result;
}

void goto_programt::create_badnode(
  map< instructionst::const_iterator, Node * > &NodeMap,
  map< int, Node * > &LabelMap,
  std::ostream &out,
  instructionst::const_iterator it,
  vector<Node*> &beforenodes,
  StmtType st_type ) const
{
  Node * newbadnode = new BadNode;
  //cout << "New bad node created:" << newbadnode << endl;
  if( it->is_target() )
  {
    // see if the label exists or not
    //cout << "Target number of this node:" << it->target_number << endl;
    if( LabelMap.find(it->target_number) == LabelMap.end() )
    {
      // create a new label node
      Node * newlabelnode = new UniNode;
      ((UniNode*)newlabelnode)->next = NULL;
      LabelMap.insert( pair<int, Node *>(it->target_number, newlabelnode) );
      ((UniNode*)newlabelnode)->st = st_Label;
      Expr * var_result = new VarExpr;
      int tn = it->target_number;
      //cout << "Label node:" << it->target_number << endl;
      strcpy( ((VarExpr*)var_result)->x , i2string(tn).c_str() );
      ((UniNode*)newlabelnode)->e1 = var_result;
      ((UniNode*)newlabelnode)->e2 = NULL;
    }
    // now link the label node to this node
    ((BadNode*)newbadnode)->before.push_back( LabelMap[it->target_number] );
    ((UniNode*)(LabelMap[it->target_number]))->next = newbadnode;
    //cout << "*: " << ((UniNode*)(LabelMap[it->target_number]))->next
    //     << " now linked to label " << LabelMap[it->target_number] << endl;
  }
  for( int i =0; i < beforenodes.size(); i++ )
  {
    if( typeid( *(beforenodes.at(i)) ) == typeid( UniNode ) )
    {
      ((UniNode*)beforenodes.at(i))->next = newbadnode;
      //cout << "*: " << ((UniNode*)beforenodes.at(i)) << " now linked to " << newbadnode << endl;
    }
    else if( typeid( *(beforenodes.at(i)) ) == typeid( BinNode ) )
    {
      ((BinNode*)beforenodes.at(i))->_false = newbadnode;
      //cout << "*: " << ((BinNode*)beforenodes.at(i)) << " now linked to " << newbadnode << endl;
    }
    //else cout << "WARNING: can not identify type id"  << endl;
    else cout << "UNKNOW17" << endl;
  }
  ((BadNode*)newbadnode)->before = beforenodes;
  // No Next Node
  NodeMap[it] = newbadnode;
  return;
}

void goto_programt::create_unarynode(
  map<string, string> &struct_information,
  const class namespacet &ns,
  const irep_idt &identifier,
  map< instructionst::const_iterator, Node * > &NodeMap,
  map< int, Node * > &LabelMap,
  std::ostream &out,
  instructionst::const_iterator it,
  vector<Node*> &beforenodes,
  StmtType st_type,
  string LabelName ) const
{
  // Jump to next target only: create a new Uni Node
  int struct_flag = 0;
  vector<Node*> v_n;
  Node * newuninode = new UniNode;
  ((UniNode*)newuninode)->next = NULL;
  //cout << "* new uninode created: " << newuninode << endl;
  //actual_nodes.push_back( newuninode );
  if( st_type == st_Assign)
  {
    int flag;
    //cout << "Number of operands:" << ((it->code).operands()).size() << endl;
    if(((it->code).op0()).get("identifier").as_string().size() > 12){
        //if(((it->code).op0()).get("identifier").as_string().compare("c::__CPROVER_alloc_size") == 0 ){
        if(((it->code).op0()).get("identifier").as_string().compare(5,7,"CPROVER") == 0 ){
            //cout << "GETGET: " <<((it->code).op0()).get("identifier").as_string() << endl;
            flag = 1;
        }
    }
    else{
        flag = 2;
    }
    //else if(((it->code).op0()).get("identifier").as_string().compare("c::__CPROVER_alloc_size") == 0 ){
    //}
    //cout << "GETGET: " <<((it->code).op0()).get("identifier").as_string() << endl;
        //cout << "information 0 == " << (it->code).op0() << endl;
        //cout << "information 1 == " << (it->code).op1() << endl;
    if((it->code).op0().id() == "symbol" && (it->code).op0().type().id() == "symbol" && (it->code).op1().id() == "symbol" && (it->code).op1().type().id() == "symbol"){
        //cout << "SYMBOL = " << (it->code).op0().get("identifier").as_string() << endl;
        //cout << "SYMBOL = " << (it->code).op0().type().id() << endl;
        string s_type = (it->code).op0().type().get("identifier").as_string().substr(7);
        //cout << "SYMBOL = " << s_type << " " << (it->code).op0() << endl;
        map<string, map<string, string> >::iterator itm;
        map<string, string>::iterator itmm;
        vector<string> v_s;
        for(itm = struct_info.begin(); itm != struct_info.end(); itm++){
            if(itm->first.compare(s_type) == 0){
                RecursiveGetMember(struct_info, itm, v_s);
                //test v_s
                /*for(int i1 = 0; i1 < v_s.size(); i1++){
                    cout << "v_s = " << v_s[i1] << endl;
                }*/
                //cout << "0identifier = " << (it->code).op0().get("identifier").as_string() << endl;
                int oi1, oi2;
                for(int i1 = 0, i2 = 0; i1 < (it->code).op0().get("identifier").as_string().size(); i1++){
                    if(i2 == 8){
                        oi1 = i1;
                        break;
                    }
                    if((it->code).op0().get("identifier").as_string()[i1] == ':'){
                        i2 = i2 + 1;
                    }
                }
                for(int i1 = 0, i2 = 0; i1 < (it->code).op1().get("identifier").as_string().size(); i1++){
                    if(i2 == 8){
                        oi2 = i1;
                        break;
                    }
                    if((it->code).op1().get("identifier").as_string()[i1] == ':'){
                        i2 = i2 + 1;
                    }
                }
                //cout << "sub = " << (it->code).op0().get("identifier").as_string().substr(oi1) << endl;
                for(int i1 = 0; i1 < v_s.size(); i1++){
                    string es0 = (it->code).op0().get("identifier").as_string().substr(oi1) + "." + v_s[i1];
                    string es1 = (it->code).op1().get("identifier").as_string().substr(oi2) + "." + v_s[i1];
                    //cout << "es0 = " << es0 << " es1 = " << es1 << endl;
                    if(i1 == v_s.size()-1){
                        Expr *ex0, *ex1;
                        ex0 = new VarExpr; strcpy(((VarExpr*)ex0)->x, es0.c_str());
                        ex1 = new VarExpr; strcpy(((VarExpr*)ex1)->x, es1.c_str());
                        ((UniNode*)newuninode)->e1 = ex0;
                        ((UniNode*)newuninode)->e2 = ex1;
                        v_n.push_back(newuninode);
                    }
                    else{
                        Expr *ex0, *ex1;
                        ex0 = new VarExpr; strcpy(((VarExpr*)ex0)->x, es0.c_str());
                        ex1 = new VarExpr; strcpy(((VarExpr*)ex1)->x, es1.c_str());
                        Node* xnode = new UniNode;
                        ((UniNode*)xnode)->e1 = ex0;
                        ((UniNode*)xnode)->e2 = ex1;
                        ((UniNode*)xnode)->st = st_type;
                        v_n.push_back(xnode);
                    }
                    /*if(i1 == 0){
                       cout << "v_n " << i1 << " " << ((VarExpr*)(((UniNode*)(v_n[0]))->e1))->x << endl;
                       cout << "v_n " << i1 << " " << ((VarExpr*)(((UniNode*)(v_n[0]))->e2))->x << endl;
                    }
                    if(i1 == 1){
                       cout << "v_n " << i1-1 << " " << ((VarExpr*)(((UniNode*)(v_n[0]))->e1))->x << endl;
                       cout << "v_n " << i1-1 << " " << ((VarExpr*)(((UniNode*)(v_n[0]))->e2))->x << endl;
                       cout << "v_n " << i1 << " " << ((VarExpr*)(((UniNode*)(v_n[1]))->e1))->x << endl;
                       cout << "v_n " << i1 << " " << ((VarExpr*)(((UniNode*)(v_n[1]))->e2))->x << endl;
                    }*/
                }
                //cout << "v_n " << v_n.size() << " v_s " << v_s.size() << endl;
                //for(int i1 = 0; i1 < (int)v_n.size(); i1++){
                    //cout << "v_n " << i1 << " " << ((VarExpr*)(((UniNode*)(*v_n[i1]))->e1))->x << endl;
                    //cout << "v_n " << i1 << " " << ((VarExpr*)(((UniNode*)(*v_n[i1]))->e2))->x << endl;
                //}
                for(int i1 = 0; i1 < (int)v_n.size(); i1++){
                    if(i1 < v_n.size()-1){
                        ((UniNode*)(v_n[i1]))->next = (v_n[i1+1]);
                    }
                    else{
                    }
                    if(i1 == 0){
                        (v_n[i1])->before.push_back( NodeMap[it] );
                    }
                    else{
                        ((UniNode*)(v_n[i1]))->before.push_back(v_n[i1-1]);
                    }
                }
                /*for(itmm = itm->second.begin(); itmm != itm->second.end(); itmm++){
                  //((UniNode*)newuninode)->e1 = handle_exprCFA( flag, ns, identifier, (it->code).op0() );
                  //育維用it->target去記錄要存的下一個點
                  cout << "first = " << itmm->first << " second = " << itmm->second << endl;
                }*/
            }
        }
        struct_flag = 1;
    }
    else if((it->code).op0().type().id() == "fixedbv" && (it->code).op1().type().id() == "fixedbv"){
        //cout << "op1 = " << (it->code).op1() << endl;
        ((UniNode*)newuninode)->e1 = handle_exprCFA( flag, ns, identifier, (it->code).op0() );
        ((UniNode*)newuninode)->e2 = handle_exprCFA( flag, ns, identifier, (it->code).op1() );
    }
    else{
        ((UniNode*)newuninode)->e1 = handle_exprCFA( flag, ns, identifier, (it->code).op0() );
        ((UniNode*)newuninode)->e2 = handle_exprCFA( flag, ns, identifier, (it->code).op1() );
    }
    //}//GET QUESTION
  }
  else if( st_type == st_FUNC_Call &&((it->code).operands()).size()!=0 )
  {
    // e1: lhs, op2: actualparameters
    //cout << "Number of operands:" << ((it->code).operands()).size() << endl;
    ((UniNode*)newuninode)->e1 = handle_exprCFA(0, ns, identifier, (it->code).op0());
    ((UniNode*)newuninode)->e2 = handle_exprCFA(0, ns, identifier, (it->code).op1());
    //((UniNode*)newuninode)->e1 = handle_exprCFA( ((it->code).op1()), false );
    //((UniNode*)newuninode)->e2 = handle_exprCFA( ((it->code).op2()), false );
    for(exprt::operandst::const_iterator 
        t =(it->code).op2().operands().begin(); \
        t!=(it->code).op2().operands().end(); t++)
    {
      ((UniNode*)newuninode)->actualpara.push_back(handle_exprCFA( 0, ns, identifier, *t ));
    }
  }
  else if( st_type == st_Return )
  {
    //cout << "execute here2 !!! " << (it->code).No_operands() << endl;//question5
    //string return_error = (it->code).get("operands").as_string();
    //cout << "execute here2 !!! [" << return_error << "]" << endl;//question5
    //cout << "execute here2 !!! " << (it->code).has_operands() << endl;//question5
    if((it->code).No_operands() == 0){// Question quake
        Expr *dumpReturn;
        dumpReturn = new IntExpr;
        ((IntExpr*)dumpReturn)->i = 1;
        ((UniNode*)newuninode)->e1 = dumpReturn;
        ((UniNode*)newuninode)->e2 = NULL;
    }
    else{
        ((UniNode*)newuninode)->e1 = handle_exprCFA(0, ns, identifier, (it->code).op0());
        ((UniNode*)newuninode)->e2 = NULL;
    }
  }
  else if( st_type == st_Label )
  {
    string declare = from_expr(ns, identifier, it->code);
    Expr * var_result = new VarExpr;
    strcpy( ((VarExpr*)var_result)->x , LabelName.c_str() );
    ((UniNode*)newuninode)->e1 = var_result;
    ((UniNode*)newuninode)->e2 = NULL;
  }
  ((UniNode*)newuninode)->st = st_type;
  //((UniNode*)newuninode)->e2 = handle_exprCFA( (it->code).op2(), false );
  // if this node is a target
  if( it->is_target() )
  {
    // see if the label exists or not
    //cout << "Target number of this node:" << it->target_number << endl;
    if( LabelMap.find(it->target_number) == LabelMap.end() )
    {
      // create a new label node
      Node * newlabelnode = new UniNode;
      ((UniNode*)newlabelnode)->next = NULL;
      LabelMap.insert( pair<int, Node *>(it->target_number, newlabelnode) );
      ((UniNode*)newlabelnode)->st = st_Label;
      Expr * var_result = new VarExpr;
      int tn = it->target_number;
      //cout << "Label node created:" << it->target_number << ": " << newlabelnode << endl;
      strcpy( ((VarExpr*)var_result)->x , i2string(tn).c_str() );
      ((UniNode*)newlabelnode)->e1 = var_result;
      ((UniNode*)newlabelnode)->e2 = NULL;
    }
    // now link the label node to this node
    ((UniNode*)newuninode)->before.push_back( (Node*)LabelMap[it->target_number] );
    ((UniNode*)(LabelMap[it->target_number]))->next = newuninode;
    //cout << "*: " << newuninode << " now linked to label" << LabelMap[it->target_number] << endl;
  }
  // Create a dummy node
  //Node * newdummynode = new UniNode;
  //((UniNode*)newdummynode)->next = NULL;
  // Add this nodeas a before of the dummynode
  //((Node*)newdummynode)->before.push_back( newuninode );
  // link all before to this node
  //cout << "Size of before nodes:" << beforenodes.size() << endl;
  for( int i =0; i < beforenodes.size(); i++ )
  {
    if( typeid( *(beforenodes.at(i)) ) == typeid( UniNode ) )
    {
      if(struct_flag == 1){
          ((UniNode*)beforenodes.at(i))->next = v_n[0];
      }
      else{
          ((UniNode*)beforenodes.at(i))->next = newuninode;
      }
      //cout << "*: " << ((UniNode*)beforenodes.at(i)) << " now linked to " << newuninode << endl;
    }
    else if( typeid( *(beforenodes.at(i)) ) == typeid( BinNode ) )
    {
      ((BinNode*)beforenodes.at(i))->_false = newuninode;
      //cout << "*: " << ((BinNode*)beforenodes.at(i)) << " now linked to " << newuninode << endl;
    }
    //else cout << "WARNING: can not identify type id"  << endl;
  }
  ((UniNode*)newuninode)->before = beforenodes;
  //((UniNode*)newuninode)->next = newdummynode;
  //cout << "*: " << ((UniNode*)newuninode) << " now linked to " << newdummynode << endl;
  // Create a new entry to the NodeMap
  instructionst::const_iterator nextit = it;
  nextit++;
  if( nextit != instructions.end() )
  {
    if(NodeMap.find(nextit) == NodeMap.end() )
    {
      // next instruction never touched, create a new entry
      Node * newdummynode = new UniNode;
      ((UniNode*)newdummynode)->next = NULL;
      // Add this nodeas a before of the dummynode
      //((Node*)newdummynode)->before.push_back( newuninode );
      NodeMap.insert( pair< instructionst::const_iterator, Node * >(nextit, newdummynode) );
      //cout << "next instruction is: " << newdummynode << endl;
    }
    //else // someone already assign this, mostly label nodes creation
    //{
    /*if(struct_flag == 1){
        ((UniNode*)newuninode)->next = NodeMap[nextit];
        NodeMap[nextit]->before.push_back( newuninode );
        struct_flag = 0;
    }
    else{*/
        ((UniNode*)newuninode)->next = NodeMap[nextit];
        NodeMap[nextit]->before.push_back( newuninode );
    //cout << "next instruction is: " << NodeMap[nextit] << endl;
    //}
    //}
  }
  /*if(struct_flag == 1){
      NodeMap[it] = *v_n[0];
      cout << "newuninode = " << ((VarExpr*)(((UniNode*)newuninode)->e1))->x << " v_n = " << ((VarExpr*)(((UniNode*)(*v_n[0]))->e1))->x << endl;
      struct_flag = 0;
  }
  else{*/
      NodeMap[it] = newuninode;
  //}
  //
  return;
}


std::ostream& goto_programt::output_instructionCFA(
  map<string, string> &struct_information,
  const class namespacet &ns,
  const irep_idt &identifier,
  map< instructionst::const_iterator, Node * > &NodeMap,
  map< int, Node * > &LabelMap,
  //vector< Node * > &actual_nodes,
  std::ostream &out,
  instructionst::const_iterator it) const
{
  int BadNodeFlag = 0;
  //cout << it->location.as_string() << endl;
  // get dummy node from NodeMap
  if( NodeMap.find(it) == NodeMap.end() )
  {
    // this line will be skipped.
    //cout << "One line skipped." << endl;
  }
  else{
  //cout << "Translating code in position: ";
  if(!it->location.is_nil()){
    //cout << it->location.as_string();
  }
  else{
    //cout << "no specified location";
    //cout << ":" << endl;
  }
  if(!it->labels.empty())
  {
    //out << "Labels:";
    for(instructiont::labelst::const_iterator
        l_it=it->labels.begin();
        l_it!=it->labels.end();
        l_it++)
    {
      //cout << " " << *l_it;
    }
    //cout << endl;
  }
  //cout << "* Original node:" << NodeMap[it] << endl;
  // get all previous from dummy node
  vector<Node*> beforenodes = (NodeMap[it])->before;
  // check Labels and see if it is a Bad Node
  if(!it->labels.empty())
  {
    //out << "*Labels:";
    for(instructiont::labelst::const_iterator
        l_it=it->labels.begin();
        l_it!=it->labels.end();
        l_it++)
    {
      if( name2string((*l_it)) == "ERROR" )
      {
        // create bad node
        //create_badnode( NodeMap, LabelMap, out, it, beforenodes, st_Label );
        BadNodeFlag = 1;
        //return out;
      }
      //cout << name2string((*l_it)) << "  ";
      //out << " " << *l_it;
    }
  }
  // look at it's type and then look ahead
  switch(it->type)
  {
    case NO_INSTRUCTION_TYPE:
      //out << "WARNING: NO INSTRUCTION TYPE SET" << std::endl;
      break;
    case GOTO:
    {
      //cout << "Binary node case reached." << endl;
      // if guard is true, goto the target
      if(!it->guard.is_true())
      {
        //cout << "Binary node case reached." << endl;
        // create a new Binary node
        Node * newbinnode = new BinNode;
        //cout << "* new Binnode created: " << newbinnode << endl;
        ((BinNode*)newbinnode)->_true = NULL;
        ((BinNode*)newbinnode)->_false = NULL;
        ((BinNode*)newbinnode)->p = handle_propCFA( ns, identifier, it->guard );
        //NodeMap[it]->second = newbinnode;
        // if this node is a target
        if( it->is_target() )
        {
          // see if the label exists or not
          //cout << "Target number of this node:" << it->target_number << endl;
          if( LabelMap.find(it->target_number) == LabelMap.end() )
          {
            if(BadNodeFlag == 0){
            // create a new label node
            Node * newlabelnode = new UniNode;
            //cout << "* new Labelnode created: " << newlabelnode << endl;
            ((UniNode*)newlabelnode)->next = NULL;
            LabelMap.insert( pair<int, Node *>(it->target_number, newlabelnode) );
            ((UniNode*)newlabelnode)->st = st_Label;
            // label node: created as a var expr with label as string
            Expr * var_result = new VarExpr;
            int tn = it->target_number;
            //cout << "Label node:" << it->target_number << endl;
            strcpy( ((VarExpr*)var_result)->x , i2string(tn).c_str() );
            ((UniNode*)newlabelnode)->e1 = var_result;
            ((UniNode*)newlabelnode)->e2 = NULL;
            }
            else{
                Node * newlabelnode = new BadNode;
                LabelMap.insert( pair<int, Node *>(it->target_number, newlabelnode) );
            }
          }
          // now link the label node to this node 
          ((BinNode*)newbinnode)->before.push_back( (Node*)LabelMap[it->target_number] );
          ((UniNode*)(LabelMap[it->target_number]))->next = newbinnode;
          //cout << "*: " << LabelMap[it->target_number]  << " now linked to " << newbinnode << endl;
        }
        // see targets for _true link
        for(instructiont::targetst::const_iterator
          gt_it=it->targets.begin();
          gt_it!=it->targets.end();
          gt_it++)
        {
          // see if the label exists or not
          if( LabelMap.find((*gt_it)->target_number) == LabelMap.end() )
          {
            if(BadNodeFlag == 0){
            // create a new label node
            Node * newlabelnode = new UniNode;
            //cout << "* new Labelnode created: " << newlabelnode << endl;     
            ((UniNode*)newlabelnode)->next = NULL;
            LabelMap.insert( pair<int, Node *>((*gt_it)->target_number, newlabelnode) );
            ((UniNode*)newlabelnode)->st = st_Label;
            Expr * var_result = new VarExpr;
            int tn = (*gt_it)->target_number;
            //cout << "Label node:" << (*gt_it)->target_number << endl;
            strcpy( ((VarExpr*)var_result)->x , i2string(tn).c_str() );
            ((UniNode*)newlabelnode)->e1 = var_result;
            ((UniNode*)newlabelnode)->e2 = NULL;
            if( NodeMap.find( (*gt_it) ) == NodeMap.end() )
            {
              // if the new dummy node not found in the NodeMap
              Node * newdummynode = new UniNode;
              ((UniNode*)newdummynode)->next = NULL;
              NodeMap.insert( pair< instructionst::const_iterator, Node * >( (*gt_it), newdummynode) );
              ((UniNode*)(newlabelnode))->next = newdummynode;
              newdummynode->before.push_back( newlabelnode );        
            }
            }
          }
          // now link the label node to this node
          ((UniNode*)LabelMap[(*gt_it)->target_number])->before.push_back(newbinnode);
          ((BinNode*)newbinnode)->_true = LabelMap[(*gt_it)->target_number];
          //cout << "*: " << newbinnode << " now linked to label" << LabelMap[(*gt_it)->target_number] << endl;
        }
        // Create a new dummy node and add it to this node's false
        //Node * newdummynode = new UniNode;
        //((UniNode*)newdummynode)->next = NULL;
        // Add this node as a before of the dummy node
        //((Node*)newdummynode)->before.push_back( newbinnode );
        // link all before to this node
        for( int i =0; i < beforenodes.size(); i++ )
        {
          if( typeid( *(beforenodes.at(i)) ) == typeid( UniNode ) )
          {
            ((UniNode*)beforenodes.at(i))->next = newbinnode;
            //cout << "*: " << ((UniNode*)beforenodes.at(i)) << " now linked to " << newbinnode << endl;
          }         
          else if( typeid( *(beforenodes.at(i)) ) == typeid( BinNode ) )
          { 
            ((BinNode*)beforenodes.at(i))->_false = newbinnode;
            //cout << "*: " << ((BinNode*)beforenodes.at(i)) << " now linked to " << newbinnode << endl;
          }
        }
        ((BinNode*)newbinnode)->before = beforenodes;
        //((BinNode*)newbinnode)->_false = newdummynode;
        // Add this entry to NodeMap
        instructionst::const_iterator nextit = it;
        nextit++;
        if( nextit != instructions.end() )       
        {
          if(NodeMap.find(nextit) == NodeMap.end() )
          {
            Node * newdummynode = new UniNode;
            ((UniNode*)newdummynode)->next = NULL;
            //((Node*)newdummynode)->before.push_back( newbinnode );
            NodeMap.insert( pair< instructionst::const_iterator, Node * >(nextit, newdummynode) );
            //((BinNode*)newbinnode)->_false = newdummynode;
            //cout << "next instruction is: " << newdummynode << endl;
          }
          //else // someone already assign this, mostly label nodes
          //{
            //NodeMap[nextit]->before.push_back( newbinnode );
            //((BinNode*)newbinnode)->_false = NodeMap[nextit];
            //cout << "next instruction is: " << NodeMap[nextit] << endl;
          //}
          ((BinNode*)newbinnode)->_false = NodeMap[nextit];
          NodeMap[nextit]->before.push_back( newbinnode );        
          //cout << "next instruction is: " << NodeMap[nextit] << endl;
        }
        // Update NodeMap
        NodeMap[it] = newbinnode;
      }
      else
      {
        // A unary case: directly GOTO
        //cout << "Uniary node case reached." << endl;
        // Jump to next target only: create a new Uni Node
        Node * newuninode = new UniNode;
        ((UniNode*)newuninode)->st = st_Goto;
        Expr * var_result = new VarExpr;
        int tn =(*(it->targets.begin()))->target_number;
        strcpy( ((VarExpr*)var_result)->x , i2string(tn).c_str() );
        ((UniNode*)newuninode)->e1 = var_result;
        ((UniNode*)newuninode)->e2 = NULL;
        //cout << "* new uninode created: " << newuninode << endl;
        ((UniNode*)newuninode)->next = NULL;
        //actual_nodes.push_back( newuninode );
        // if this node is a target
        if( it->is_target() )
        {
          // see if the label exists or not
          if( LabelMap.find(it->target_number) == LabelMap.end() )
          {
            // create a new label node
            Node * newlabelnode = new UniNode;
            //cout << "* new Labelnode created: " << newlabelnode << endl;
            ((UniNode*)newlabelnode)->next = NULL;
            LabelMap.insert( pair<int, Node *>(it->target_number, newlabelnode) );
            ((UniNode*)newlabelnode)->st = st_Label;
            Expr * var_result = new VarExpr;
            int tn = it->target_number;
            //cout << "Label node:" << it->target_number << endl;
            strcpy( ((VarExpr*)var_result)->x , i2string(tn).c_str() );
            ((UniNode*)newlabelnode)->e1 = var_result;
            ((UniNode*)newlabelnode)->e2 = NULL;
          }
          // now link the label node to this node
          ((UniNode*)newuninode)->before.push_back( (Node*)LabelMap[it->target_number] );
          ((UniNode*)(LabelMap[it->target_number]))->next = newuninode;
          //cout << "*: " << newuninode << " now linked to label" << LabelMap[it->target_number] << endl;
        }
        // see targets for _true link
        for(instructiont::targetst::const_iterator
          gt_it=it->targets.begin();
          gt_it!=it->targets.end();
          gt_it++)
        {
          // see if the label exists or not
          if( LabelMap.find((*gt_it)->target_number) == LabelMap.end() )
          {
            // create a new label node
            Node * newlabelnode = new UniNode;
            //cout << "* new Labelnode created: " << newlabelnode << endl;
            ((UniNode*)newlabelnode)->next = NULL;
            LabelMap.insert( pair<int, Node *>((*gt_it)->target_number, newlabelnode) );
            ((UniNode*)newlabelnode)->st = st_Label;  
            Expr * var_result = new VarExpr;
            int tn = (*gt_it)->target_number;
            //cout << "Label node:" << (*gt_it)->target_number << endl;
            strcpy( ((VarExpr*)var_result)->x , i2string(tn).c_str() );
            ((UniNode*)newlabelnode)->e1 = var_result;
            ((UniNode*)newlabelnode)->e2 = NULL;
            if( NodeMap.find( (*gt_it) ) == NodeMap.end() )
            {
              // if the new dummy node not found in the NodeMap
              Node * newdummynode = new UniNode;
              ((UniNode*)newdummynode)->next = NULL;
              NodeMap.insert( pair< instructionst::const_iterator, Node * >( (*gt_it), newdummynode) );
              ((UniNode*)(newlabelnode))->next = newdummynode;
              newdummynode->before.push_back( newlabelnode );
              //cout << "Dummynode " << newdummynode << " created for label node " << newlabelnode << endl;
            }
          }
          // now link the label node to this node
          ((UniNode*)LabelMap[(*gt_it)->target_number])->before.push_back(newuninode);
          ((UniNode*)newuninode)->next = LabelMap[(*gt_it)->target_number];
          //cout << "*: " << newuninode << " now linked to label " << LabelMap[(*gt_it)->target_number] << endl;
        }
        // link all before to this node
        for( int i =0; i < beforenodes.size(); i++ )
        {
          if( typeid( *(beforenodes.at(i)) ) == typeid( UniNode ) )
          {
            ((UniNode*)beforenodes.at(i))->next = newuninode;
            //cout << "*: " << ((UniNode*)beforenodes.at(i)) << " now linked to " << newuninode << endl;
          }
          else if( typeid( *(beforenodes.at(i)) ) == typeid( BinNode ) )
          {
            ((BinNode*)beforenodes.at(i))->_false = newuninode;
            //cout << "*: " << ((BinNode*)beforenodes.at(i)) << " now linked to " << newuninode << endl;
          }
        }
        // Update NodeMap
        NodeMap[it] = newuninode;
      }
      break;
    }
    case RETURN:
    case OTHER:
    case DEAD:
    {
        //cout << "execute here1 !!! " << endl;
      //cout << "Uninode case reached(Return)." << endl;
      create_unarynode(struct_information, ns, identifier, NodeMap, LabelMap, out, it, beforenodes, st_Return, "DEAD" );
      break;
    }
    case FUNCTION_CALL:
    {
      //cout << "Uninode case reached.(FUNCTION CALL)" << endl;
      create_unarynode(struct_information, ns, identifier, NodeMap, LabelMap, out, it, beforenodes, st_FUNC_Call, "FUNC_Call" );
      break;
    }
    case DECL:
    {
      //cout << "Uninode case(Decl) reached." << endl;
      //cout << "identifier = " << identifier << endl;
      string ex_s = from_expr(ns, identifier, it->code);
      pair<string, string> p_struct;
      if(ex_s.compare(2,6,"struct") == 0){
          stringstream ss (stringstream::in | stringstream::out);
          ss << ex_s;
          string type_s;
          ss >> type_s;//struct
          ss >> type_s;//type
          p_struct.second = type_s; 
          ss >> type_s;//name;
          type_s.erase(type_s.size()-1, 1);//name
          p_struct.first = type_s;
          struct_information.insert(p_struct);
          //test
          /*cout << "test_struct" << endl;
          map<string, string>::iterator its;
          for(its = struct_information.begin(); its != struct_information.end(); its++){
              cout << its->first << " => " << its->second << endl;
          }*/
      }
      create_unarynode(struct_information, ns, identifier, NodeMap, LabelMap, out, it, beforenodes, st_Label, "DECL" );
      break;
    }
    case ASSIGN:
    { 
      //cout << "Uninode case(Assign) reached." << endl;
      //if(((it->code).op0()).get("identifier").as_string().size() > 12){
          //if(((it->code).op0()).get("identifier").as_string().compare("c::__CPROVER_alloc_size") == 0 ){
      //    if(((it->code).op0()).get("identifier").as_string().compare(5,7,"CPROVER") == 0 ){
      //        cout << "GETGET: " <<((it->code).op0()).get("identifier").as_string() << endl;
      //    }
      //}
      //else{
          create_unarynode(struct_information, ns, identifier, NodeMap, LabelMap, out, it, beforenodes, st_Assign, "ASSIGN" );
      //}
      break;
    }
    case END_FUNCTION:
    {
      //cout << "Uninode case(END_FUNCTION) reached.(WARNING: NOT fully SUPPORTED YET)" << endl;
      create_unarynode(struct_information, ns, identifier, NodeMap, LabelMap, out, it, beforenodes, st_Label, "END_FUNCTION" );
      break;
    }
    case ASSUME:
    {
      //cout << "Uninode case(ASSUME) reached.(WARNING: NOT SUPPORTED YET)" << endl;
      create_unarynode(struct_information, ns, identifier, NodeMap, LabelMap, out, it, beforenodes, st_Label, "ASSUME" );
      break;
    }
    case ASSERT:
    {
      //cout << "Uninode case(ASSERT) reached.(WARNING: NOT SUPPORTED YET)" << endl;
      create_unarynode(struct_information, ns, identifier, NodeMap, LabelMap, out, it, beforenodes, st_Label, "ASSERT" );
      break;
    }
    case LOCATION:
    {
      //cout << "Uninode case(LOCATION) reached.(WARNING: NOT SUPPORTED YET)" << endl;
      create_unarynode(struct_information, ns, identifier, NodeMap, LabelMap, out, it, beforenodes, st_Label, "LOCATION" );
      break;
    }
    case THROW:
    {
      //cout << "Uninode case(THROW) reached.(WARNING: NOT SUPPORTED YET)" << endl;
      create_unarynode(struct_information, ns, identifier, NodeMap, LabelMap, out, it, beforenodes, st_Label, "THROW" );
      break;
    }
    case CATCH:
    {
      //cout << "Uninode case(CATCH) reached.(WARNING: NOT SUPPORTED YET)" << endl;
      create_unarynode(struct_information, ns, identifier, NodeMap, LabelMap, out, it, beforenodes, st_Label, "CATCH" );
      break;
    }
    case ATOMIC_BEGIN:
    {
      //cout << "Uninode case(ATOMIC_BEGIN) reached.(WARNING: NOT SUPPORTED YET)" << endl;
      create_unarynode(struct_information, ns, identifier, NodeMap, LabelMap, out, it, beforenodes, st_Label, "ATOMIC_BEGIN" );
      break;
    }
    case ATOMIC_END:
    {
      //cout << "Uninode case(ATOMIC_END) reached.(WARNING: NOT SUPPORTED YET)" << endl;
      create_unarynode(struct_information, ns, identifier, NodeMap, LabelMap, out, it, beforenodes, st_Label, "ATOMIC_END" );
      break;
    }
    case START_THREAD:
    {
      //cout << "Uninode case(START_THREAD) reached.(WARNING: NOT SUPPORTED YET)" << endl;
      create_unarynode(struct_information, ns, identifier, NodeMap, LabelMap, out, it, beforenodes, st_Label, "START_THREAD" );
      break;
    }
    case END_THREAD:
    {
      //cout << "Uninode case(END_THREAD) reached.(WARNING: NOT SUPPORTED YET)" << endl;
      create_unarynode(struct_information, ns, identifier, NodeMap, LabelMap, out, it, beforenodes, st_Label, "END_THREAD" );
      break;
    }
    default:
    {
      //cout << "Default case reached. WARNING: YOU MAY REACHED UNSPECIFIED INSTRUCTION" << endl;
      // This is a terminal node: change all before nodes to NULL
      for( int i =0; i < beforenodes.size(); i++ )
      {
        if( typeid( *(beforenodes.at(i)) ) == typeid( UniNode ) )
        {
          ((UniNode*)beforenodes.at(i))->next = NULL;
        }
        else if( typeid( *(beforenodes.at(i)) ) == typeid( BinNode ) )
        {
          ((BinNode*)beforenodes.at(i))->_false = NULL;
        }
      }
      break;
    }
  }
  }
  //
  //cout << "GOOD: this Instruction has been successfully processed." << endl << endl;
  return out;
}


/*******************************************************************\

Function: goto_programt::output_instruction

  Inputs:

 Outputs:

 Purpose:

\*******************************************************************/

std::ostream& goto_programt::output_instruction(
  const class namespacet &ns,
  const irep_idt &identifier,
  std::ostream& out,
  instructionst::const_iterator it) const
{
  //out << "        // " << it->location_number << " ";
  //out << "* Code in ";

  if(!it->location.is_nil()){
    //out << it->location.as_string();
  }
  else{
    //out << "no location";
  }

  //out << ":" << std::endl;
 
  if(!it->labels.empty())
  {
    //out << "        // Labels:";
    for(instructiont::labelst::const_iterator
        l_it=it->labels.begin();
        l_it!=it->labels.end();
        l_it++)
    {
      //out << " " << *l_it;
    }
    
    //out << std::endl;
  }
  //cout << endl << "Targets:" << endl;

  if(it->is_target()){
    //out << std::setw(6) << it->target_number << ": ";
  }
  else{
    //out << "        ";
  }
  
  switch(it->type)
  {
  case NO_INSTRUCTION_TYPE:
    //out << "NO INSTRUCTION TYPE SET" << std::endl;
    break;
  
  case GOTO:
    if(!it->guard.is_true())
    {
      //out << "iF "
      //    << from_expr(ns, identifier, it->guard)
      //    << " THEN ";
    }

    //out << "GOTO ";
    
    for(instructiont::targetst::const_iterator
        gt_it=it->targets.begin();
        gt_it!=it->targets.end();
        gt_it++)
    {
      //if(gt_it!=it->targets.begin()) out << ", ";
      //out << (*gt_it)->target_number;
    }
      
    //out << std::endl;
    break;
    
  case RETURN:
  case OTHER:
  case DECL:
  case DEAD:
  case FUNCTION_CALL:
  case ASSIGN:
    //out << from_expr(ns, identifier, it->code) << std::endl;
    break;
    
  case ASSUME:
  case ASSERT:
    //if(it->is_assume()){
      //out << "ASSUME ";
    //{
    //else{
      //out << "ASSERT ";
    //}
      
    {
      //out << from_expr(ns, identifier, it->guard);
    
      const irep_idt &comment=it->location.get(ID_comment);
      //if(comment!="") out << " // " << comment;
    }
      
    //out << std::endl;
    break;
    
  case SKIP:
    //out << "SKIP" << std::endl;
    break;
    
  case END_FUNCTION:
    //out << "END_FUNCTION" << std::endl;
    break;
    
  case LOCATION:
    //out << "LOCATION" << std::endl;
    break;
    
  case THROW:
    //out << "THROW" << std::endl;
    break;
    
  case CATCH:
    //out << "CATCH" << std::endl;
    break;
    
  case ATOMIC_BEGIN:
    //out << "ATOMIC_BEGIN" << std::endl;
    break;
    
  case ATOMIC_END:
    //out << "ATOMIC_END" << std::endl;
    break;
    
  case START_THREAD:
    //out << "START THREAD ";

    if(it->targets.size()==1)
      //out << it->targets.front()->target_number;
    
    //out << std::endl;
    break;
    
  case END_THREAD:
    //out << "END THREAD" << std::endl;
    break;
    
  default:
    throw "UNKNOW";
  }
  //out << std::endl; 
 
  return out;  
}

/*******************************************************************\

Function: goto_programt::get_decl_identifiers

  Inputs:

 Outputs:

 Purpose:

\*******************************************************************/

void goto_programt::get_decl_identifiers(
  decl_identifierst &decl_identifiers) const
{
  forall_goto_program_instructions(it, (*this))
  {
    if(it->is_decl())
    {
      assert(it->code.get_statement()==ID_decl);
      assert(it->code.operands().size()==1);
      const symbol_exprt &symbol_expr=to_symbol_expr(it->code.op0());
      decl_identifiers.insert(symbol_expr.get_identifier());
    }
  }
} 

/*******************************************************************\

Function: operator<

  Inputs:

 Outputs:

 Purpose:

\*******************************************************************/

bool operator<(const goto_programt::const_targett i1,
               const goto_programt::const_targett i2)
{
  const goto_programt::instructiont &_i1=*i1;
  const goto_programt::instructiont &_i2=*i2;
  return &_i1<&_i2;
}

/*******************************************************************\

Function: parse_lhs_read

  Inputs:

 Outputs:

 Purpose:

\*******************************************************************/

void parse_lhs_read(const exprt &src, std::list<exprt> &dest)
{
  if(src.id()==ID_dereference)
  {
    assert(src.operands().size()==1);
    dest.push_back(src.op0());
  }
  else if(src.id()==ID_index)
  {
    assert(src.operands().size()==2);
    dest.push_back(src.op1());
    parse_lhs_read(src.op0(), dest);
  }
  else if(src.id()==ID_member)
  {
    assert(src.operands().size()==1);
    parse_lhs_read(src.op0(), dest);
  }
  else if(src.id()==ID_if)
  {
    assert(src.operands().size()==3);
    dest.push_back(src.op0());
    parse_lhs_read(src.op1(), dest);
    parse_lhs_read(src.op2(), dest);
  }
}

/*******************************************************************\

Function: expressions_read

  Inputs:

 Outputs:

 Purpose:

\*******************************************************************/

std::list<exprt> expressions_read(
  const goto_programt::instructiont &instruction)
{
  std::list<exprt> dest;

  switch(instruction.type)
  {
  case ASSUME:
  case ASSERT:
  case GOTO:
    dest.push_back(instruction.guard);
    break;
  
  case RETURN:
    if(to_code_return(instruction.code).return_value().is_not_nil())
      dest.push_back(to_code_return(instruction.code).return_value());
    break;
  
  case FUNCTION_CALL:
    {
      const code_function_callt &function_call=
        to_code_function_call(instruction.code);
      forall_expr(it, function_call.arguments())
        dest.push_back(*it);
      if(function_call.lhs().is_not_nil())
        parse_lhs_read(function_call.lhs(), dest);
    }
    break;
  
  case ASSIGN:
    {
      const code_assignt &assignment=to_code_assign(instruction.code);
      dest.push_back(assignment.rhs());
      parse_lhs_read(assignment.lhs(), dest);
    }
    break;
  
  default:;
  }
  
  return dest;
}

/*******************************************************************\

Function: expressions_written

  Inputs:

 Outputs:

 Purpose:

\*******************************************************************/

std::list<exprt> expressions_written(
  const goto_programt::instructiont &instruction)
{
  std::list<exprt> dest;

  switch(instruction.type)
  {
  case FUNCTION_CALL:
    {
      const code_function_callt &function_call=
        to_code_function_call(instruction.code);
      if(function_call.lhs().is_not_nil())
        dest.push_back(function_call.lhs());
    }
    break;
  
  case ASSIGN:
    dest.push_back(to_code_assign(instruction.code).lhs());
    break;
  
  default:;
  }
  
  return dest;
}

/*******************************************************************\

Function: get_objects_read

  Inputs:

 Outputs:

 Purpose:

\*******************************************************************/

void objects_read(
  const exprt &src,
  std::list<exprt> &dest) 
{
  if(src.id()==ID_symbol)
    dest.push_back(src);
  else if(src.id()==ID_address_of)
  {
    // don't traverse!
    assert(src.operands().size()==1);
    dest.push_back(src);
    objects_read(src.op0(), dest);
  }
  else
  {
    forall_operands(it, src)
      objects_read(*it, dest);
  }
}

/*******************************************************************\

Function: objects_read

  Inputs:

 Outputs:

 Purpose:

\*******************************************************************/

std::list<exprt> objects_read(
  const goto_programt::instructiont &instruction)
{
  std::list<exprt> expressions=expressions_read(instruction);

  std::list<exprt> dest;
  
  forall_expr_list(it, expressions)
    objects_read(*it, dest);
  
  return dest;
}

/*******************************************************************\

Function: objects_written

  Inputs:

 Outputs:

 Purpose:

\*******************************************************************/

void objects_written(
  const exprt &src,
  std::list<exprt> &dest)
{
  if(src.id()==ID_if)
  {
    assert(src.operands().size()==3);
    objects_written(src.op1(), dest);
    objects_written(src.op2(), dest);
  }
  else
    dest.push_back(src);
}

/*******************************************************************\

Function: objects_written

  Inputs:

 Outputs:

 Purpose:

\*******************************************************************/

std::list<exprt> objects_written(
  const goto_programt::instructiont &instruction)
{
  std::list<exprt> expressions=expressions_written(instruction);

  std::list<exprt> dest;
  
  forall_expr_list(it, expressions)
    objects_written(*it, dest);
  
  return dest;
}
